refactor(prover): centralize u64 limb decomposition (dword_wl/dword_hl)#697
Open
MauroToscano wants to merge 2 commits into
Open
refactor(prover): centralize u64 limb decomposition (dword_wl/dword_hl)#697MauroToscano wants to merge 2 commits into
MauroToscano wants to merge 2 commits into
Conversation
…rd_hl Replace the open-coded little-endian limb decomposition repeated across ~20 trace tables with two helpers in tables::types: dword_wl(x) -> [FE; 2] 2x32-bit limbs (DWordWL) dword_hl(x) -> [FE; 4] 4x16-bit limbs (DWordHL) Kept as plain prover functions rather than methods on the generic Table: the limb width is field-size-specific (a 32-bit limb only fits because Goldilocks is ~64-bit, since FE::from reduces mod p), so this logic belongs in the prover, not the field-generic storage type. Only consecutive-column FE writes were converted (consecutiveness checked in each cols module). Parametric column indices, DWordWHH/byte/nibble groupings, sign-extended arrays, and bus-value arrays were left as-is. Byte-identical: prover lib tests pass 416 (the 5 ecsm failures are pre-existing/environmental, identical on main). fmt + clippy clean. Supersedes #693 (1/2).
28f3d42 to
38a3b73
Compare
…ites Address review on #697: route the last few open-coded decompositions through dword_wl/dword_hl so the split is truly single-source: - ecsm::write_dword_wl now calls dword_wl(value) internally (keeps its parametric-column flexibility, drops the duplicated 2x32 split) - cpu res loop -> zip cols::RES with dword_hl(res) - memw old_timestamp loop -> dword_wl(op.old_timestamp[i]) Byte-identical: prover lib tests 416 pass (the 5 ecsm failures are pre-existing/environmental); fmt + clippy clean.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Centralizes the repeated
u64 -> little-endian limbdecomposition that was open-coded across ~20 VM trace tables into two helpers inprover/src/tables/types.rs:Call sites destructure and assign, so only the decomposition is dedup'd — the column assignments stay explicit:
Why plain functions, not methods on
TableThe limb width is field-size-specific:
FE::from(u64)reduces mod p, so a 32-bit limb is only faithful because Goldilocks is ~64-bit. On a ~31-bit field (e.g. BabyBear) it would silently corrupt. So this belongs in the prover (which fixes the field), not the field-genericTable<F>storage type.Scope
Converted only consecutive-column FE writes (verified consecutive in each
colsmodule). Deliberately left as-is: parametric column indices (cols_i[..],lo_col),DWordWHH(Word+Half+Half) groups, byte/nibble splits, sign-extended[u64; 8]arrays (mul), and[u16;4]/[u32;4]bus/struct arrays.Correctness
Byte-identical trace output.
cargo test -p lambda-vm-prover --lib: 416 passed; the only 5 failures are*ecsm*prove tests that fail identically onmain(pre-existingUnknownSyscallin the executor, upstream of trace generation).cargo fmt+cargo clippyclean.Relationship to #693
Supersedes #693 (the original
set_limbs_*approach) — part 1 of 2. Part 2 is a separate PR that makesTable.dataprivate and routes the post-build multiplicity updaters throughset_main(fixing a latent disk-spill hazard).